#include "icut.h"

//=============================================================================
//  EXTERNAL TABLE
//=============================================================================
extern unsigned short belookup[4][256][4];
inline unsigned short be( unsigned short s, unsigned short in , unsigned short c)
{
   return belookup[s][in][c];
}
extern char bits_in_16bits[];
inline int bitcount (unsigned int n)
{
   return bits_in_16bits [n&0xffff] 
       +  bits_in_16bits [n>>16] ;
}

//=============================================================================
//  Static functions 
//=============================================================================
static unsigned short mask[5] = {1,0x3,0xF,0xFF,0xFFFF};
static unsigned short  CutSeq[16][3] = 
{  
   {3,3,6},    
          {3,2,6},{2,3,6},      
   {2,2,5},              {3,1,4},{1,3,4},    
          {2,1,4},{1,2,4},              {3,0,4},{0,3,4},
   {1,1,4},              {2,0,4},{0,2,4},
          {1,0,3},{0,1,3},
   {0,0,2} 
};
// sort to unique order 
class CutCmp
{
   const unsigned short size; 
   public:
   CutCmp( unsigned short s ):size( s ){}
   bool operator()( const Cut & a , const Cut & b )const
   {
      for( unsigned i = 0 ; i < size ; ++ i)
      {
         if( ( a.node[i] ) < ( b.node[i] ) )return true;
         if( ( b.node[i] ) < ( a.node[i] ) )return false;
      }
      return false;
   }
};
static bool cutEq( const Cut & a , const Cut & b , unsigned short size)
{
   if( a.fun != b.fun ) return false;
   for( unsigned i = 0 ; i < size ; ++ i)
      if( a.node[i]  !=  b.node[i]  )return false;

   return true;
}
class CutEq
{
   const unsigned short size;
   public:
   inline bool operator()( const Cut & a, const Cut & b )const {return cutEq(a,b,size) ; }
   CutEq( unsigned short s ):size(s){}
};
struct CutAND
{
   const fun_t sa;
   const fun_t sb;
   const short asize;
   const short bsize;

   unsigned cutand( unsigned * o , fun_t & funo , const unsigned * a , fun_t fa ,const unsigned * b , fun_t fb );
};
unsigned CutAND::cutand( unsigned * o , fun_t & funo , const unsigned * a , fun_t funa , const unsigned * b , fun_t funb )
{
   unsigned char oi = 0 , as = asize , ai = 0 , bs = bsize , bi = 0;
   do
   {
      if( *a < *b )
      {
         if( bs == DBSIZE )return 0;
         *o++ = *a++ , ++oi , ++ai , funb = be( bs++ , funb , bi++ );
         if( ai == as )
         {
            if( oi + bs - bi > DBSIZE ) return 0;
            while( bi != bs ) *o++ = *b++ , ++oi , ++bi , funa = be( as++ , funa , ai++ );
            funo = ((sa)^funa) & ((sb)^(funb)) & mask[oi];
            return oi;
         }
      }else if( *b < *a )
      {
         if( as == DBSIZE ) return 0;
         *o++ = *b++ , ++oi , ++bi , funa = be( as++ , funa , ai++ ); 
         if( bi == bs )
         {
            if( oi + as - ai > DBSIZE ) return 0;
            while( ai != as ) *o++ = *a++ , ++oi, ++ai , funb = be( bs++ , funb , bi ++ );
            funo = ((sa)^funa) & ((sb)^(funb)) & mask[oi];
            return oi;
         }
      }else
      {
         *o++ = *a++ , ++b; ++oi , ++ bi, ++ ai;
         if( ai == as )
         {
            if( oi + bs - bi > DBSIZE ) return 0;
            while( bi != bs ) *o++ = *b++ , ++oi , ++bi , funa = be( as++ , funa , ai++ );
            funo = ((sa)^funa) & ((sb)^(funb)) & mask[oi];
            return oi;
         }
         if( bi == bs )
         {
            if( oi + as - ai > DBSIZE ) return 0;
            while( ai != as ) *o++ = *a++ , ++oi, ++ai , funb = be( bs++ , funb , bi ++ );
            funo = ((sa)^funa) & ((sb)^(funb)) & mask[oi];
            return oi;
         }
      }
      if( oi == DBSIZE) return 0 ;
   }while(1);
   return oi;
}
static void cutand(   const CutArray & aary , 
                      const CutArray & bary , 
                            CutArray & cary , unsigned x , AigLit aptr , AigLit bptr )
{
   Cut ct[DBSIZE][256];
   unsigned ptr[DBSIZE]={1,0};

   ct[0][0] = Cut( x );
  
   Cut tmp;

   for( unsigned i = 0 ; i < 16 ; ++ i )
   {
      if( CutSeq[i][0] >= DBSIZE || CutSeq[i][1] >= DBSIZE ) continue;

      const CutSet & a = aary[ CutSeq[i][0] ] ;
      const CutSet & b = bary[ CutSeq[i][1] ] ;

      unsigned sizea = CutSeq[i][0] + 1 ;
      unsigned sizeb = CutSeq[i][1] + 1 ;

      unsigned sizec;
      unsigned sa = std::min( a.size , 16);
      unsigned sb = std::min( b.size , 16);

      CutAND ca = { -sign( aptr ) , -sign( bptr ) , sizea , sizeb };

      for( unsigned m = 0 ; m < sa ; ++ m )
         for( unsigned n = 0 ; n < sb ; ++n )
         {
            tmp.signature = a[m].signature | b[n].signature;
            if( bitcount( tmp.signature ) > 4 )continue;
            sizec = ca.cutand( tmp.node , tmp.fun , a[m].node , a[m].fun , b[n].node , b[n].fun );
            if( sizec  )
            {
               if( ptr[sizec-1] >= 256 ) continue;

//               tmp.nodes = 1 + (unsigned)(( 1.0*sizec/(sizea+sizeb) )*(a[m].nodes+b[n].nodes));
               ct[sizec-1][ ptr[sizec-1] ] = tmp;
               ptr[sizec-1] +=1;
            }
         }
   }
   for( unsigned i = 0 ; i < DBSIZE ; ++i)
   {
      if( ptr[i] == 0 ) continue;
      std::sort( ct[i] , ct[i] + ptr[i] , CutCmp( i+1 ) );
      unsigned y = 0 ;
      for( x = 1 ; x < ptr[i]  ; ++ x )
         if( ! cutEq( ct[i][y] , ct[i][x] , i+1) ) ct[i][++y] = ct[i][x];
      switch( i )
      {
         case 0: ptr[i]=1; break;
         case 1: ptr[i]=y+1; break;
         case 2: ptr[i]=std::min(y+1,(unsigned)64); break;
         case 3: ptr[i]=std::min(y+1,(unsigned)64); break;
      }
   }
   for( unsigned i = 0 ; i < DBSIZE ; ++i )
   {
      cary[i].allocate( ptr[i] );
      std::copy( ct[i] , ct[i] + ptr[i] , cary[i].dat );
   }
}
void InfoCut::set_base( unsigned i )
{
   _cut[i][0].allocate( 1 );
   _cut[i][1].size =  _cut[i][2].size = _cut[i][3].size = 0;
   _cut[i][0][0].init( i );
}
void InfoCut::validation()
{
   CktInfo::validation();
   _cut.resize( size() );
}
void InfoCut::create_base()
{
   if( _cut.size() == 0 ) _cut.growTo( size() );
   for( unsigned i = 0 ; i < _andFlag ; ++ i )
      set_base( i );
   _cut[0][0][0].fun = 0x0;
}
void InfoCut::update( unsigned i )
{
   assert( i >= _andFlag && setted(i) == false );
   AigLit p[2] = {eqIn(i,0),eqIn(i,1)};
   unsigned v[2] = {var(p[0]),var(p[1])};
   
   if(!setted( v[0] ) )update( v[0] );
   if(!setted( v[1] ) )update( v[1] );

   cutand( _cut[ v[0] ] , _cut[ v[1] ] , _cut[ i ] , i , p[0], p[1] );
}

